\begin{tabbing}
es{-}interface{-}local{-}state\=\{i:l\}\+
\\[0ex](${\it es}$; $f$; ${\it base}$; $X$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if $e$ $\in_{b}$ $X$\+
\\[0ex]then $f$(es{-}local{-}prior{-}state\{i:l\}(${\it es}$; $f$; ${\it base}$; $X$; $e$),$X$($e$))
\\[0ex]else es{-}local{-}prior{-}state\=\{i:l\}\+
\\[0ex](${\it es}$; $f$; ${\it base}$; $X$; $e$)
\-\\[0ex]fi 
\-
\end{tabbing}